(* This file is part of IsoType.
 *
 * IsoType is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * IsoType is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with IsoType.  If not, see <http://www.gnu.org/licenses/>.
 *)

open OptionMonad

let iso flags typ typ' = 
  let rec aux typ typ' renaming = aux_phase_1 typ typ' renaming

  and aux_phase_1 typ typ' renaming =
    let coords = Type.flatten_pairs typ
    and coords' = Type.flatten_pairs typ' in
      ListAux.unordered_unify aux_phase_2 coords coords' renaming

  and aux_phase_2 typ1 typ2 renaming =
    let (typ1_domains, typ1') = Type.flatten_arrows typ1
    and (typ2_domains, typ2') = Type.flatten_arrows typ2 in
      aux_phase_3 typ1' typ2' renaming
      >>= ListAux.unordered_unify aux typ1_domains typ2_domains

  and aux_phase_3 typ typ' renaming = 
    match typ, typ' with
	(* BEWARE: TWO VARIABLES MUST BE UNIFIED EVEN IF EQUAL,
	   BECAUSE THEY ACTUALLY REFER TO DIFFERENT TYPES AND WE MUST
	   BE SURE THAT EVERY VARAIBLE IS UNIFIED EXACTLY ONCE *)
	Type.Var tvar, Type.Var tvar' when List.mem (tvar, tvar') renaming -> Some renaming
      | Type.Var tvar, Type.Var tvar' when List.mem_assoc tvar renaming || List.mem_assoc tvar' renaming -> None
      | Type.Var tvar, Type.Var tvar' -> Some ((tvar, tvar') :: (tvar', tvar) :: renaming)
      | Type.Predefined (typs, qname), Type.Predefined (typs', qname') -> Some renaming
      | Type.Predefined (typs, qname), Type.Predefined (typs', qname') when qname = qname' -> 
	  ListAux.ordered_unify aux typs typs' renaming
      | Type.Record fields, Type.Record fields' ->
	  ListAux.unordered_unify aux_field fields fields' renaming
      | Type.Algebraic ctors, Type.Algebraic ctors' ->
	  ListAux.unordered_unify aux_ctor ctors ctors' renaming
      | Type.Rec (tvar1, typ1), Type.Rec (tvar2, typ2) ->
	  let tvar = Type.Var (Type.get_var ()) in
	    aux (Type.subst tvar1 tvar typ1) (Type.subst tvar2 tvar typ2) renaming
	      (* BEWARE: RECURSION VARIABLES WILL BE UNIFIED, HENCE
		 THEY WILL OCCUR IN THE RENAMING *)
      | Type.Arrow _, _
      | _, Type.Arrow _
      | Type.Pair _, _
      | _, Type.Pair _ ->
	  prerr_endline (Printf.sprintf "INTERNAL ERROR: %s\n%s" (Type.string_of_type typ) (Type.string_of_type typ'));
	  assert false (* IMPOSSIBLE *)
      | _ -> None

  and aux_ctor (Type.Constructor (_, typ)) (Type.Constructor (_, typ')) = aux typ typ'
    
  and aux_field (Type.Field (_, typ)) (Type.Field (_, typ')) = aux typ typ'
  in
  let t0 = Sys.time () in
  let res = aux (Type.snf flags typ) (Type.snf flags typ') [] in
  let t1 = Sys.time () in
    match res with
	None -> false
      | Some renaming ->
	  if Flags.debug flags then
	    begin
	      prerr_endline (Printf.sprintf "IN\n%s\n===?===\n%s" (Type.string_of_type typ) (Type.string_of_type typ'));
	      prerr_string "[ ";
	      List.iter
		(fun (tvar, tvar') ->
		   prerr_string (Printf.sprintf "(%s,%s) " (Type.string_of_var tvar) (Type.string_of_var tvar'))
		)
		renaming;
	      prerr_endline "]";
	      prerr_endline (Printf.sprintf "OUT YES %2.3f" (t1 -. t0));
	      flush stderr
	    end;
	  true
